open Utils.Pervasive
open Utils.Error
open Utils.StringSpecial
open Syntax
open Pointers
open Core
open PrintExpr
open Binding
open GPUtils 
open GtkText


let error_log str =
		let file_name =  "errors.txt" in 
		let file_channel = open_out_gen 
			[Open_creat; Open_append; Open_creat] 
			666 file_name in
		
		output_string file_channel str;
		flush file_channel;
		close_out file_channel

let make_win_title expr = 
	match expr with
	| Ty (_, None) -> "An unamed type:"
	| Ty (_, Some name) -> "A name (\"" ^ name ^ "\") for the type:"
	| Te (te, None)-> "An unamed term:" 
	| Te (te, Some name) -> "A name (\"" ^ name ^ "\") for the term:" 
		
let view_fvar_routine ctx expr ( ) = ( )(*
	let window = GWindow.window 
		~border_width:10 
		~title:"free vars" () in
		un (window #connect#destroy ~callback:window#destroy);
		let box1 = GPack.vbox ~packing:window#add () in
	
		let vars = GBin.frame ~label:"Vars..." ~packing:box1#pack () in
		let text = match expr with
		|Ty _ -> "Expression is a type"
		|Te (te, _) -> 
			String.concat "\n" 
			(List.map (fun te -> string_of_term ctx te Alpha) (free_term_vars ctx te))
		in
		un(GMisc.label
		~text:text ~packing:vars#add ( ));	
	window#show( )	*)
		
let rec make_expr_panel env expr ctx = 	
	let panel title = 
		let pan = GBin.frame ~label:(title^ "...") ~packing:env#add ( ) in
		GPack.vbox ~width:580 ~packing:pan#add ( ) in
	
	let evalPanel = panel "Expression" in
		let box_eval = GPack.hbox ~packing:evalPanel#add () in
		let box_eval_left = GPack.vbox ~packing:box_eval#add () in
		let expr_label = GText.view 
			~width:300 
			~height:300 
			~border_width:3 
			~wrap_mode:`WORD
			~packing:box_eval_left#add( ) 	in 
	
	let reset_expr_label( ) = 
		expr_label#buffer#set_text
		("(" ^ string_of_expr ctx expr Compact ^ ")") in
	reset_expr_label( );
	let unevaluated_expression ( ) = parse_string (expr_label#buffer#get_text( )) ctx in
	let evaluated_expression ( ) = 
			match unevaluated_expression ( ) with
			| Ty (ty , _) -> Ty (ty, None)
			| Te (te, _) -> Te (normalize ctx te, None) in

	let box_eval_right = GPack.vbox ~packing:box_eval#add () in
	let eval_button = GButton.button ~label:"eval" 
		~packing:box_eval_right#pack () in	
	let eval_routine ( ) =
		let new_expr =  evaluated_expression ( ) in 
		show_expr_window ctx new_expr ( ) in
	un (eval_button#connect#clicked ~callback:eval_routine);
	match expr with
	| Te (te, _) -> 
		let box_typeof = GPack.hbox ~packing:evalPanel#add () in
		let ty = typeof ctx te in
		let box_typeof_left = GPack.vbox ~packing:box_typeof#add () in
		let type_label = GEdit.entry 
		~editable:false
		~text:"" 
		~width:500 
		~packing:box_typeof_left#add () in
		type_label#set_text ("Of type: " ^ (string_of_type ctx ty Alpha));
		
		let box_typeof_right = GPack.vbox ~packing:box_typeof#add () in
		let view_type = GButton.button ~label:"Open" 
		~packing:box_typeof_right#pack () in
		un (view_type#connect#clicked ~callback:(show_expr_window ctx (Ty (ty, None))))		
	|_->()
	
		
and show_expr_window ctx expr ( ) = 
	
	let win expr = show_expr_window ctx expr in

	let str expr = 
		(try string_of_expr ctx expr Alpha
		with |_-> prf "error in  string_of_expr"; "error str") in
	
	let title = make_win_title expr in
	let window = GWindow.window 
		~border_width:10 
		~title:title () in
		un (window #connect#destroy ~callback:window#destroy);
		(*un(close_button#connect#clicked ~callback:window#destroy);*)
	
	let hBox = GPack.hbox ~packing:window#add () in
	let boxMenu = GPack.vbox  ~packing:hBox#add () in
	
	make_expr_panel boxMenu expr ctx;
		
	(*let panel title = 
		let pan = GBin.frame ~label:(title^ "...") ~packing:boxMenu#pack ( ) in
		GPack.vbox ~width:580 ~packing:pan#add ( ) in
	
	let repPanel = panel "Representation..." in
	
	un(GMisc.label ~text:("\n  De Bruijn: " ^ str expr)
		~packing:repPanel#add ());
		
	let compPanel = panel "Other information..." in 
	
	un(GMisc.label
		~text:("Complexity: " ^ string_of_int (complexity_of_expr expr))
		~packing:compPanel#add ());
	let view_fvar_button = GButton.button ~label:"See free variables" 
		~packing:compPanel#pack () in
	un (view_fvar_button#connect#clicked ~callback:(view_fvar_routine ctx expr));
	
	
	
	let evalPanel = panel "Evaluation Tests..." in
		let box_eval = GPack.hbox ~packing:evalPanel#add () in
		let box_eval_left = GPack.vbox ~packing:box_eval#add () in
		let expr_label = GEdit.entry 
		~editable:true
		~text:"" 
		~width:500 
		~packing:box_eval_left#add () in
		
	let reset_expr_label( ) = expr_label#set_text (string_of_expr ctx expr Compact) in
	reset_expr_label( );
		
	let unevaluated_expression ( ) = parse_string (expr_label#text) ctx in
		let evaluated_expression ( ) = 
			match unevaluated_expression ( ) with
			| Ty (ty , _) -> Ty (ty, None)
			| Te (te, _) -> Te (normalize ctx te, None) in

		
		
	(*Evaluation tests*)
	let box_eval_right = GPack.vbox ~packing:box_eval#add () in
	let eval_button = GButton.button ~label:"eval" 
		~packing:box_eval_right#pack () in	
	let eval_routine ( ) =
		let new_expr =  evaluated_expression ( ) in 
		reset_expr_label( );
		show_expr_window ctx new_expr ( ) in
	un (eval_button#connect#clicked ~callback:eval_routine);
	
	
	
	
	*)
	window#show( )
	
	
	
	
	
	
	
	